package list3;

class Data {}

class SomeOne {
	public void work(/*@ readonly @*/ List l) {
		// The list is readonly, but we can create a local
		// iterator that we can modify via "next".
		
		/*@ peer @*/ ListIter it = l.iterator();
		
		while( it.hasCurrent() ) {
			System.out.println("Data: " + it.getCurrent());
			it.next();
			
			// however, calling "remove" would violate the precondition.
			// it.remove();
		}
	}
}

public class ListDemo {
	public void run() {
		/*@ rep @*/ List l = new /*@ rep @*/ List();
		l.add( new Data() );
		l.add( new Data() );
		
		// we have a RW reference to the list and
		// can therefore create a RW iterator.
		/*@ rep @*/ ListIter itrw = l.iterator();
		if( itrw.hasCurrent() ) {
			// the precondition of remove is met.
			itrw.remove();
		}
		
		/*@ peer @*/ SomeOne so = new /*@ peer @*/ SomeOne();
		so.work( l );
		
		System.out.println("Done");
	}
	
	public static void main(String[] args) {
		new ListDemo().run();
	}
}
